ePMC

Benchmark
Model:firewire v.2 (MDP)
Parameter(s)explicit_timer = False, delay = 36, deadline = 200
Property:time_max (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files firewire.false.jani --model-input-type jani --property-input-names time_max --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const delay=36,deadline=200
Execution
Walltime:10.750996351242065s
Return code:0
Relative Error:1.0393021249315069e-05
Log
assertions-disabled
model-checking
analysing-property time_max
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 27487 27486
build-model-states-explored 82776 55290
build-model-states-explored 141256 58480
build-model-states-explored 211279 70023
build-model-done 212268 4
iterating
iterating-progress-unbounded 468 0.0027900974262032863 1
iterating-progress-unbounded 978 1.3455550573233802E-4 2
iterating-progress-unbounded 1488 1.3590577618126242E-5 3
iterating-progress-unbounded 1998 1.8434933081599557E-6 4
iterating-done 2308 4
num-states-in-filter 1 "initial"
printing-all-filter-results
print-filter 0 0 364.996206547244
model-checking-done 10
command-check-result-is 364.996206547244 time_max